$\forall$$a$:Id, $p$:FinProbSpace, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $P$:(State(${\it ds}$)$\rightarrow\mathbb{B}$).
\\[0ex](precondition $a$:Outcome($p$) is $P$:State(${\it ds}$) {-}$>$ Bool) $\in$ MsgA